let V be RealLinearSpace; :: thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded
set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);
ex C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) st
for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds
( C "\/" A = C & A "\/" C = C )
proof
reconsider C = (Omega). V as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
take C ; :: thesis: for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds
( C "\/" A = C & A "\/" C = C )
let A be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); :: thesis: ( C "\/" A = C & A "\/" C = C )
reconsider W = A as Subspace of V by Def3;
thus C "\/" A = ((Omega). V) + W by Def7
.= C by Th11 ; :: thesis: A "\/" C = C
hence A "\/" C = C ; :: thesis: verum
end;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded ; :: thesis: verum