let V be RealLinearSpace; :: 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 ;

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

then A1:
Bottom S = Z
by Lm19;let A be Element of S0; :: thesis: A "/\" Z0 = Z0

reconsider W = A as Subspace of V by Def3;

thus A "/\" Z0 = W /\ ((0). V) by Def8

.= Z0 by Th18 ; :: thesis: verum

end;reconsider W = A as Subspace of V by Def3;

thus A "/\" Z0 = W /\ ((0). V) by Def8

.= Z0 by Th18 ; :: thesis: verum

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

then A2:
Top S = I
by Lm20;let A be Element of S1; :: thesis: A "\/" I1 = (Omega). V

reconsider W = A as Subspace of V by Def3;

thus A "\/" I1 = W + ((Omega). V) by Def7

.= (Omega). V by Th11 ; :: thesis: verum

end;reconsider W = A as Subspace of V by Def3;

thus A "\/" I1 = W + ((Omega). V) by Def7

.= (Omega). V by Th11 ; :: thesis: verum

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

hence
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented
; :: thesis: verumlet 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 = the strict Linear_Compl of W /\ W by Def8

.= Bottom S by A1, Th37 ;

B "\/" A = the strict Linear_Compl of W + W by Def7

.= Top S by A2, Th36 ;

hence B is_a_complement_of A by A3, Lm18; :: thesis: verum

end;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 = the strict Linear_Compl of W /\ W by Def8

.= Bottom S by A1, Th37 ;

B "\/" A = the strict Linear_Compl of W + W by Def7

.= Top S by A2, Th36 ;

hence B is_a_complement_of A by A3, Lm18; :: thesis: verum