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; :: 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; :: thesis: verum
end;
hence "/\" (Y,C) [= "/\" (X,C) by Th34; :: thesis: verum