let V be RealUnitarySpace; :: thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented
reconsider S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) as 01_Lattice by Th57;
reconsider S0 = S as 0_Lattice ;
reconsider S1 = S as 1_Lattice ;
reconsider Z = (0). V, I = (Omega). V as Element of S by Def3;
reconsider Z0 = Z as Element of S0 ;
reconsider I1 = I as Element of S1 ;

now :: thesis: for A being Element of S0 holds A "/\" Z0 = Z0

let A be Element of S0; :: thesis: A "/\" Z0 = Z0
reconsider W = A as Subspace of V by Def3;
thus A "/\" Z0 = (SubMeet V) . (A,Z0) by LATTICES:def 2
.= W /\ ((0). V) by Def8
.= Z0 by Th18 ; :: thesis: verum

end;

then A1: Bottom S = Z by RLSUB_2:64;

now :: thesis: for A being Element of S1 holds A "\/" I1 = (Omega). V

let A be Element of S1; :: thesis: A "\/" I1 = (Omega). V
reconsider W = A as Subspace of V by Def3;
thus A "\/" I1 = (SubJoin V) . (A,I1) by LATTICES:def 1
.= W + ((Omega). V) by Def7
.= UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Th11
.= (Omega). V by RUSUB_1:def 3 ; :: thesis: verum

end;

then A2: Top S = I by RLSUB_2:65;

now :: thesis: for A being Element of S ex B being Element of S st B is_a_complement_of A

let A be Element of S; :: thesis: ex B being Element of S st B is_a_complement_of A
reconsider W = A as Subspace of V by Def3;
set L = the strict Linear_Compl of W;
reconsider B9 = the strict Linear_Compl of W as Element of S by Def3;
take B = B9; :: thesis: B is_a_complement_of A
A3: B "/\" A = (SubMeet V) . (B,A) by LATTICES:def 2
.= the strict Linear_Compl of W /\ W by Def8
.= Bottom S by A1, Th37 ;
B "\/" A = (SubJoin V) . (B,A) by LATTICES:def 1
.= the strict Linear_Compl of W + W by Def7
.= UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Th36
.= Top S by A2, RUSUB_1:def 3 ;
hence B is_a_complement_of A by A3, LATTICES:def 18; :: thesis: verum

end;

hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented by LATTICES:def 19; :: thesis: verum