set I = F;
set A = (subrelstr F) opp+id ;
let x, y be Element of ((subrelstr F) opp+id); :: according to WAYBEL_0:def 1,WAYBEL_0:def 6 :: thesis: ( not x in [#] ((subrelstr F) opp+id) or not y in [#] ((subrelstr F) opp+id) or ex b₁ being Element of the carrier of ((subrelstr F) opp+id) st
( b₁ in [#] ((subrelstr F) opp+id) & x <= b₁ & y <= b₁ ) )
A1: the carrier of (subrelstr F) = F by YELLOW_0:def 15;
A2: the carrier of ((subrelstr F) opp+id) = the carrier of (subrelstr F) by WAYBEL_9:def 6;
assume that
A3: x in [#] ((subrelstr F) opp+id) and
A4: y in [#] ((subrelstr F) opp+id) ; :: thesis: ex b₁ being Element of the carrier of ((subrelstr F) opp+id) st
( b₁ in [#] ((subrelstr F) opp+id) & x <= b₁ & y <= b₁ )
reconsider a = x, b = y as Element of R by A1, A2, A3, A4;
A5: RelStr(# the carrier of ((subrelstr F) opp+id), the InternalRel of ((subrelstr F) opp+id) #) = RelStr(# the carrier of ((subrelstr F) opp), the InternalRel of ((subrelstr F) opp) #) by WAYBEL_9:11;
consider c being Element of R such that
A6: c in F and
A7: a >= c and
A8: b >= c by A1, A2, WAYBEL_0:def 2;
reconsider a1 = x, b1 = y, c1 = c as Element of (subrelstr F) by A6, WAYBEL_9:def 6, YELLOW_0:def 15;
reconsider z = c as Element of ((subrelstr F) opp+id) by A2, A6, YELLOW_0:def 15;
take z ; :: thesis: ( z in [#] ((subrelstr F) opp+id) & x <= z & y <= z )
A9: a1 ~ = a1 by LATTICE3:def 6;
A10: b1 ~ = b1 by LATTICE3:def 6;
A11: c1 ~ = c1 by LATTICE3:def 6;
A12: a1 >= c1 by A7, YELLOW_0:60;
A13: b1 >= c1 by A8, YELLOW_0:60;
A14: a1 ~ <= c1 ~ by A12, LATTICE3:9;
b1 ~ <= c1 ~ by A13, LATTICE3:9;
hence ( z in [#] ((subrelstr F) opp+id) & x <= z & y <= z ) by A5, A9, A10, A11, A14; :: thesis: verum