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 A2: a in X ; :: thesis: a [= "\/" Y,C
Y is_less_than "\/" Y,C by Def21;
hence a [= "\/" Y,C by A1, A2, 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 A3: a in X ; :: thesis: "/\" Y,C [= a
"/\" Y,C is_less_than Y by Th34;
hence "/\" Y,C [= a by A1, A3, Def16; :: thesis: verum

end;

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