let C be complete Lattice; :: thesis: for a being Element of C
for X being set st a in X & X is_less_than a holds
"\/" X,C = a
let a be Element of C; :: thesis: for X being set st a in X & X is_less_than a holds
"\/" X,C = a
let X be set ; :: thesis: ( a in X & X is_less_than a implies "\/" X,C = a )
assume that
A1: a in X and
A2: X is_less_than a ; :: thesis: "\/" X,C = a
A3: "\/" X,C [= a by A2, Def21;
a [= "\/" X,C by A1, Th38;
hence "\/" X,C = a by A3, LATTICES:26; :: thesis: verum