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

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 & ("\/" the carrier of C,C) "\/" a [= "\/" the carrier of C,C ) by Th38, LATTICES:22;
hence ("\/" the carrier of C,C) "\/" a = "\/" the carrier of C,C by LATTICES:26; :: 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, LATTICES:26; :: thesis: verum

end;

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