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:8; :: thesis: verum

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:8; :: thesis: verum