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 A2, LATTICES:8; :: 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 A2, A3, LATTICES:8; :: thesis: verum

end;

then C is upper-bounded ;
hence ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) ) by A1, LATTICES:def 17; :: thesis: verum