let S1, S2 be non empty antisymmetric RelStr ; :: thesis: for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds
[x,y] >= b ) holds
( ( for c being Element of S1 st c is_<=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds
y >= d ) )
let D1 be Subset of S1; :: thesis: for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds
[x,y] >= b ) holds
( ( for c being Element of S1 st c is_<=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds
y >= d ) )
let D2 be Subset of S2; :: thesis: for x being Element of S1
for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds
[x,y] >= b ) holds
( ( for c being Element of S1 st c is_<=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds
y >= d ) )
let x be Element of S1; :: thesis: for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds
[x,y] >= b ) holds
( ( for c being Element of S1 st c is_<=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds
y >= d ) )
let y be Element of S2; :: thesis: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds
[x,y] >= b ) implies ( ( for c being Element of S1 st c is_<=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds
y >= d ) ) )
assume that
A1: ex_inf_of D1,S1 and
A2: ex_inf_of D2,S2 and
A3: for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds
[x,y] >= b ; :: thesis: ( ( for c being Element of S1 st c is_<=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds
y >= d ) )
thus for c being Element of S1 st c is_<=_than D1 holds
x >= c :: thesis: for d being Element of S2 st d is_<=_than D2 holds
y >= d
proof
A4: inf D2 is_<=_than D2 by A2, YELLOW_0:31;
let b be Element of S1; :: thesis: ( b is_<=_than D1 implies x >= b )
assume b is_<=_than D1 ; :: thesis: x >= b
then [x,y] >= [b,(inf D2)] by A3, A4, Th33;
hence x >= b by Th11; :: thesis: verum
end;
A5: inf D1 is_<=_than D1 by A1, YELLOW_0:31;
let b be Element of S2; :: thesis: ( b is_<=_than D2 implies y >= b )
assume b is_<=_than D2 ; :: thesis: y >= b
then [x,y] >= [(inf D1),b] by A3, A5, Th33;
hence y >= b by Th11; :: thesis: verum