let L be with_infima Poset; :: thesis: for x, y being Element of L holds x "/\" y = (x ~) "\/" (y ~)

let x, y be Element of L; :: thesis: x "/\" y = (x ~) "\/" (y ~)

x "/\" y <= y by YELLOW_0:23;

then A1: (x "/\" y) ~ >= y ~ by LATTICE3:9;

A2: ( ~ (x ~) = x ~ & ~ (y ~) = y ~ ) ;

then (x "/\" y) ~ >= x ~ by LATTICE3:9;

hence x "/\" y = (x ~) "\/" (y ~) by A1, A3, YELLOW_0:22; :: thesis: verum

let x, y be Element of L; :: thesis: x "/\" y = (x ~) "\/" (y ~)

x "/\" y <= y by YELLOW_0:23;

then A1: (x "/\" y) ~ >= y ~ by LATTICE3:9;

A2: ( ~ (x ~) = x ~ & ~ (y ~) = y ~ ) ;

A3: now :: thesis: for d being Element of (L opp) st d >= x ~ & d >= y ~ holds

(x "/\" y) ~ <= d

x "/\" y <= x
by YELLOW_0:23;(x "/\" y) ~ <= d

let d be Element of (L opp); :: thesis: ( d >= x ~ & d >= y ~ implies (x "/\" y) ~ <= d )

assume ( d >= x ~ & d >= y ~ ) ; :: thesis: (x "/\" y) ~ <= d

then ( ~ d <= x & ~ d <= y ) by A2, Th1;

then A4: ~ d <= x "/\" y by YELLOW_0:23;

(~ d) ~ = ~ d ;

hence (x "/\" y) ~ <= d by A4, LATTICE3:9; :: thesis: verum

end;assume ( d >= x ~ & d >= y ~ ) ; :: thesis: (x "/\" y) ~ <= d

then ( ~ d <= x & ~ d <= y ) by A2, Th1;

then A4: ~ d <= x "/\" y by YELLOW_0:23;

(~ d) ~ = ~ d ;

hence (x "/\" y) ~ <= d by A4, LATTICE3:9; :: thesis: verum

then (x "/\" y) ~ >= x ~ by LATTICE3:9;

hence x "/\" y = (x ~) "\/" (y ~) by A1, A3, YELLOW_0:22; :: thesis: verum