let C be complete Lattice; :: thesis: ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) )

set j = "\/" ( the carrier of C,C);

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

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) )

then
C is upper-bounded
;( ("\/" ( 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;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

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