Step 
Hyp 
Ref 
Expression 
1 

ocvlsp.v 
⊢ 𝑉 = ( Base ‘ 𝑊 ) 
2 

ocvlsp.o 
⊢ ⊥ = ( ocv ‘ 𝑊 ) 
3 
1 2

ocvocv 
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ⊆ 𝑉 ) → 𝑇 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ) 
4 
3

3adant2 
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → 𝑇 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ) 
5 
2

ocv2ss 
⊢ ( 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ⊆ ( ⊥ ‘ 𝑆 ) ) 
6 

sstr2 
⊢ ( 𝑇 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ⊆ ( ⊥ ‘ 𝑆 ) → 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) ) ) 
7 
4 5 6

syl2im 
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → ( 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) → 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) ) ) 
8 
1 2

ocvocv 
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) 
9 
8

3adant3 
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) 
10 
2

ocv2ss 
⊢ ( 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ ( ⊥ ‘ 𝑇 ) ) 
11 

sstr2 
⊢ ( 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ ( ⊥ ‘ 𝑇 ) → 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) ) ) 
12 
9 10 11

syl2im 
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → ( 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) → 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) ) ) 
13 
7 12

impbid 
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → ( 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) ↔ 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) ) ) 