let C be complete Lattice; :: thesis: for X, Y being set st X c= Y holds
( "\/" X,C [= "\/" Y,C & "/\" Y,C [= "/\" X,C )
let X, Y be set ; :: thesis: ( X c= Y implies ( "\/" X,C [= "\/" Y,C & "/\" Y,C [= "/\" X,C ) )
assume A1: X c= Y ; :: thesis: ( "\/" X,C [= "\/" Y,C & "/\" Y,C [= "/\" X,C )
X is_less_than "\/" Y,C

proof

let a be Element of C; :: according to LATTICE3:def 17 :: thesis: ( a in X implies a [= "\/" Y,C )
assume a in X ; :: thesis: a [= "\/" Y,C
then ( a in Y & Y is_less_than "\/" Y,C ) by A1, Def21;
hence a [= "\/" Y,C by Def17; :: thesis: verum

end;

hence "\/" X,C [= "\/" Y,C by Def21; :: thesis: "/\" Y,C [= "/\" X,C
"/\" Y,C is_less_than X

proof

let a be Element of C; :: according to LATTICE3:def 16 :: thesis: ( a in X implies "/\" Y,C [= a )
assume a in X ; :: thesis: "/\" Y,C [= a
then ( a in Y & "/\" Y,C is_less_than Y ) by A1, Th34;
hence "/\" Y,C [= a by Def16; :: thesis: verum

end;

hence "/\" Y,C [= "/\" X,C by Th34; :: thesis: verum