let C be complete Lattice; :: thesis: ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) )
set j = "\/" ( the carrier of C,C);
A1: now :: thesis: for a being Element of C holds
( ("\/" ( the carrier of C,C)) "\/" a = "\/" ( the carrier of C,C) & a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C) )
let a be Element of C; :: thesis: ( ("\/" ( the carrier of C,C)) "\/" a = "\/" ( the carrier of C,C) & a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C) )
A2: "\/" ( the carrier of C,C) [= ("\/" ( the carrier of C,C)) "\/" a by LATTICES:5;
A3: ("\/" ( the carrier of C,C)) "\/" a [= "\/" ( the carrier of C,C) by Th38;
hence ("\/" ( the carrier of C,C)) "\/" a = "\/" ( the carrier of C,C) by ; :: thesis: a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C)
thus a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C) by ; :: thesis: verum
end;
then C is upper-bounded ;
hence ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) ) by ; :: thesis: verum