let C be complete Lattice; ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) )
set j = "\/" ( the carrier of C,C);
A1:
now 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;
( ("\/" ( 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;
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;
verum end;
then
C is upper-bounded
;
hence
( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) )
by A1, LATTICES:def 17; verum