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

proof

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

end;

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