defpred S₁[ object , object ] means ex I being Element of (InclPoset (Ids (subrelstr B))) ex z1, z2 being Element of L st
( z1 = $1 & z2 = $2 & I in X & $2 in I & z1 <= z2 );
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: x in downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) ; :: thesis:
then reconsider x1 = x as Element of L ;
consider y1 being Element of L such that
A7: y1 >= x1 and
A8: y1 in finsups (union ((idsMap (subrelstr B)) .: X)) by A6, WAYBEL_0:def 15;
y1 in { ("\/" (V,L)) where V is finite Subset of (union ((idsMap (subrelstr B)) .: X)) : ex_sup_of V,L } by A8, WAYBEL_0:def 27;
then consider Y being finite Subset of (union ((idsMap (subrelstr B)) .: X)) such that
A9: y1 = "\/" (Y,L) and
ex_sup_of Y,L ;
A10: for z being object st z in Y holds
ex v being Element of B st S₁[z,v]

let z be object ; :: thesis:
assume z in Y ; :: thesis:
then consider J being set such that
A11: z in J and
A12: J in (idsMap (subrelstr B)) .: X by TARSKI:def 4;
consider I being object such that
I in dom (idsMap (subrelstr B)) and
A13: I in X and
A14: J = (idsMap (subrelstr B)) . I by A12, FUNCT_1:def 6;
reconsider I = I as Element of (InclPoset (Ids (subrelstr B))) by A13;
(idsMap (subrelstr B)) . I is Element of (InclPoset (Ids L)) ;
then reconsider J = J as Element of (InclPoset (Ids L)) by A14;
J is Ideal of L by YELLOW_2:41;
then reconsider z1 = z as Element of L by A11;
reconsider I1 = I as Ideal of (subrelstr B) by YELLOW_2:41;
consider I2 being Subset of L such that
A15: I1 = I2 and
A16: (idsMap (subrelstr B)) . I1 = downarrow I2 by Def11;
consider z2 being Element of L such that
A17: z2 >= z1 and
A18: z2 in I2 by A11, A14, A16, WAYBEL_0:def 15;
reconsider v = z2 as Element of B by A15, A18, YELLOW_0:def 15;
take v ; :: thesis:
take I ; :: thesis:
take z1 ; :: thesis:
take z2 ; :: thesis:
thus ( z1 = z & z2 = v & I in X & v in I & z1 <= z2 ) by A13, A15, A17, A18; :: thesis:

end;

consider g being Function of Y,B such that
A19: for z being object st z in Y holds
S₁[z,g . z] from MONOID_1:sch 1(A10);
reconsider Z = rng g as finite Subset of (subrelstr B) by YELLOW_0:def 15;
A20: dom g = Y by FUNCT_2:def 1;
A21: "\/" ((rng g),L) is_>=_than Y

let a be Element of L; :: according to LATTICE3:def 9 :: thesis:
A22: "\/" ((rng g),L) is_>=_than rng g by YELLOW_0:32;
assume A23: a in Y ; :: thesis:
then consider I being Element of (InclPoset (Ids (subrelstr B))), a1, a2 being Element of L such that
A24: a1 = a and
A25: a2 = g . a and
I in X and
g . a in I and
A26: a1 <= a2 by A19;
g . a in rng g by A20, A23, FUNCT_1:def 3;
then a2 <= "\/" ((rng g),L) by A25, A22;
hence a <= "\/" ((rng g),L) by A24, A26, YELLOW_0:def 2; :: thesis:

end;

end;

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng g ; :: thesis:
then consider b being object such that
A28: b in dom g and
A29: a = g . b by FUNCT_1:def 3;
ex I being Element of (InclPoset (Ids (subrelstr B))) ex b1, b2 being Element of L st
( b1 = b & b2 = g . b & I in X & g . b in I & b1 <= b2 ) by A19, A28;
hence a in union X by A29, TARSKI:def 4; :: thesis:

end;

end;

end;

then reconsider xl = "\/" (Z,L) as Element of (subrelstr B) ;
reconsider srg = "\/" ((rng g),(subrelstr B)) as Element of L by YELLOW_0:58;
A31: ex_sup_of Z,L by YELLOW_0:17;

end;

let b be Element of (subrelstr B); :: according to LATTICE3:def 9 :: thesis:
reconsider b1 = b as Element of L by YELLOW_0:58;
assume b in Z ; :: thesis:
then b1 <= "\/" (Z,L) by A34;
hence b <= xl by YELLOW_0:60; :: thesis:

end;

end;