let L be with_suprema Poset; :: thesis: for X, Y being Subset of L
for X', Y' being Subset of (L opp ) st X = X' & Y = Y' holds
X "\/" Y = X' "/\" Y'
let X, Y be Subset of L; :: thesis: for X', Y' being Subset of (L opp ) st X = X' & Y = Y' holds
X "\/" Y = X' "/\" Y'
let X', Y' be Subset of (L opp ); :: thesis: ( X = X' & Y = Y' implies X "\/" Y = X' "/\" Y' )
assume that
A1: X = X' and
A2: Y = Y' ; :: thesis: X "\/" Y = X' "/\" Y'
thus X "\/" Y c= X' "/\" Y' :: according to XBOOLE_0:def 10 :: thesis: X' "/\" Y' c= X "\/" Y

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X "\/" Y or a in X' "/\" Y' )
assume a in X "\/" Y ; :: thesis: a in X' "/\" Y'
then a in { (p "\/" q) where p, q is Element of L : ( p in X & q in Y ) } by YELLOW_4:def 3;
then consider x, y being Element of L such that
A3: a = x "\/" y and
A4: x in X and
A5: y in Y ;
A6: ( x ~ in X' & y ~ in Y' ) by A1, A2, A4, A5, LATTICE3:def 6;
a = (x ~ ) "/\" (y ~ ) by A3, YELLOW_7:23;
then a in { (p "/\" q) where p, q is Element of (L opp ) : ( p in X' & q in Y' ) } by A6;
hence a in X' "/\" Y' by YELLOW_4:def 4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X' "/\" Y' or a in X "\/" Y )
assume a in X' "/\" Y' ; :: thesis: a in X "\/" Y
then a in { (p "/\" q) where p, q is Element of (L opp ) : ( p in X' & q in Y' ) } by YELLOW_4:def 4;
then consider x, y being Element of (L opp ) such that
A7: a = x "/\" y and
A8: x in X' and
A9: y in Y' ;
A10: ( ~ x in X & ~ y in Y ) by A1, A2, A8, A9, LATTICE3:def 7;
a = (~ x) "\/" (~ y) by A7, YELLOW_7:24;
then a in { (p "\/" q) where p, q is Element of L : ( p in X & q in Y ) } by A10;
hence a in X "\/" Y by YELLOW_4:def 3; :: thesis: verum