let C be complete Lattice; 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; for X being set st a in X & X is_less_than a holds
"\/" (X,C) = a
let X be set ; ( 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
; "\/" (X,C) = a
A3:
"\/" (X,C) [= a
by A2, Def21;
a [= "\/" (X,C)
by A1, Th38;
hence
"\/" (X,C) = a
by A3, LATTICES:8; verum