let V be RealLinearSpace; :: thesis: LattStr(# (),(),() #) is complemented
reconsider S = LattStr(# (),(),() #) 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 = W /\ ((0). V) by Def8
.= Z0 by Th18 ; :: thesis: verum
end;
then A1: Bottom S = Z by Lm19;
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 = W + () by Def7
.= (Omega). V by Th11 ; :: thesis: verum
end;
then A2: Top S = I by Lm20;
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:
A3: B "/\" A = the strict Linear_Compl of W /\ W by Def8
.= Bottom S by ;
B "\/" A = the strict Linear_Compl of W + W by Def7
.= Top S by ;
hence B is_a_complement_of A by ; :: thesis: verum
end;
hence LattStr(# (),(),() #) is complemented ; :: thesis: verum