reconsider a = q `3 , b = q `4 as Element of L ;
set x = q `1 ;
set y = q `2 ;
defpred S₁[ Element of new_set2 A, Element of new_set2 A, set ] means ( ( $1 in A & $2 in A implies $3 = d . $1,$2 ) & ( ( ( $1 = {A} & $2 = {{A}} ) or ( $2 = {A} & $1 = {{A}} ) ) implies $3 = ((d . (q `1 ),(q `2 )) "\/" a) "/\" b ) & ( ( $1 = {A} or $1 = {{A}} ) & $2 = $1 implies $3 = Bottom L ) & ( $1 in A & $2 = {A} implies ex p9 being Element of A st
( p9 = $1 & $3 = (d . p9,(q `1 )) "\/" a ) ) & ( $1 in A & $2 = {{A}} implies ex p9 being Element of A st
( p9 = $1 & $3 = (d . p9,(q `2 )) "\/" a ) ) & ( $2 in A & $1 = {A} implies ex q9 being Element of A st
( q9 = $2 & $3 = (d . q9,(q `1 )) "\/" a ) ) & ( $2 in A & $1 = {{A}} implies ex q9 being Element of A st
( q9 = $2 & $3 = (d . q9,(q `2 )) "\/" a ) ) );
{{A}} in {{A},{{A}}} by TARSKI:def 2;
then A1: {{A}} in new_set2 A by XBOOLE_0:def 3;
A2: for p, q being Element of new_set2 A ex r being Element of L st S₁[p,q,r]

proof

let p, q be Element of new_set2 A; :: thesis: ex r being Element of L st S₁[p,q,r]
A3: ( p in A or p in {{A},{{A}}} ) by XBOOLE_0:def 3;
A4: ( q in A or q in {{A},{{A}}} ) by XBOOLE_0:def 3;
A5: ( ( ( p = {A} or p = {{A}} ) & p = q ) iff ( ( p = {A} & q = {A} ) or ( p = {{A}} & q = {{A}} ) ) ) ;
A6: not {A} in A by TARSKI:def 1;
A7: {A} <> {{A}}

proof

assume {A} = {{A}} ; :: thesis: contradiction
then {A} in {A} by TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

A8: not {{A}} in A

proof

A9: ( A in {A} & {A} in {{A}} ) by TARSKI:def 1;
assume {{A}} in A ; :: thesis: contradiction
hence contradiction by A9, ORDINAL1:3; :: thesis: verum

end;

per cases ( ( p in A & q in A ) or ( p = {A} & q = {{A}} ) or ( q = {A} & p = {{A}} ) or ( ( p = {A} or p = {{A}} ) & q = p ) or ( p in A & q = {A} ) or ( p in A & q = {{A}} ) or ( q in A & p = {A} ) or ( q in A & p = {{A}} ) ) by A3, A4, A5, TARSKI:def 2;

suppose ( p in A & q in A ) ; :: thesis: ex r being Element of L st S₁[p,q,r]

then reconsider p9 = p, q9 = q as Element of A ;
take d . p9,q9 ; :: thesis: S₁[p,q,d . p9,q9]
thus S₁[p,q,d . p9,q9] by A6, A8; :: thesis: verum

end;

suppose A10: ( ( p = {A} & q = {{A}} ) or ( q = {A} & p = {{A}} ) ) ; :: thesis: ex r being Element of L st S₁[p,q,r]

take ((d . (q `1 ),(q `2 )) "\/" a) "/\" b ; :: thesis: S₁[p,q,((d . (q `1 ),(q `2 )) "\/" a) "/\" b]
thus S₁[p,q,((d . (q `1 ),(q `2 )) "\/" a) "/\" b] by A7, A8, A10, TARSKI:def 1; :: thesis: verum

end;

suppose A11: ( ( p = {A} or p = {{A}} ) & q = p ) ; :: thesis: ex r being Element of L st S₁[p,q,r]

take Bottom L ; :: thesis: S₁[p,q, Bottom L]
thus S₁[p,q, Bottom L] by A7, A8, A11, TARSKI:def 1; :: thesis: verum

end;

suppose A12: ( p in A & q = {A} ) ; :: thesis: ex r being Element of L st S₁[p,q,r]

then reconsider p9 = p as Element of A ;
take (d . p9,(q `1 )) "\/" a ; :: thesis: S<sub>1</sub>[p,q,(d . p9,(q `1 )) "\/" a]
thus S₁[p,q,(d . p9,(q `1 )) "\/" a] by A7, A8, A12, TARSKI:def 1; :: thesis: verum

end;

suppose A13: ( p in A & q = {{A}} ) ; :: thesis: ex r being Element of L st S₁[p,q,r]

then reconsider p9 = p as Element of A ;
take (d . p9,(q `2 )) "\/" a ; :: thesis: S<sub>1</sub>[p,q,(d . p9,(q `2 )) "\/" a]
thus S₁[p,q,(d . p9,(q `2 )) "\/" a] by A7, A8, A13, TARSKI:def 1; :: thesis: verum

end;

suppose A14: ( q in A & p = {A} ) ; :: thesis: ex r being Element of L st S₁[p,q,r]

then reconsider q9 = q as Element of A ;
take (d . q9,(q `1 )) "\/" a ; :: thesis: S<sub>1</sub>[p,q,(d . q9,(q `1 )) "\/" a]
thus S₁[p,q,(d . q9,(q `1 )) "\/" a] by A7, A8, A14, TARSKI:def 1; :: thesis: verum

end;

suppose A15: ( q in A & p = {{A}} ) ; :: thesis: ex r being Element of L st S₁[p,q,r]

then reconsider q9 = q as Element of A ;
take (d . q9,(q `2 )) "\/" a ; :: thesis: S<sub>1</sub>[p,q,(d . q9,(q `2 )) "\/" a]
thus S₁[p,q,(d . q9,(q `2 )) "\/" a] by A7, A8, A15, TARSKI:def 1; :: thesis: verum

end;

end;

end;

consider f being Function of [:(new_set2 A),(new_set2 A):],the carrier of L such that
A16: for p, q being Element of new_set2 A holds S₁[p,q,f . p,q] from BINOP_1:sch 3(A2);
reconsider f = f as BiFunction of (new_set2 A),L ;
{A} in {{A},{{A}}} by TARSKI:def 2;
then A17: {A} in new_set2 A by XBOOLE_0:def 3;
A18: for u being Element of A holds
( f . {A},u = (d . u,(q `1 )) "\/" a & f . {{A}},u = (d . u,(q `2 )) "\/" a )

proof

let u be Element of A; :: thesis: ( f . {A},u = (d . u,(q `1 )) "\/" a & f . {{A}},u = (d . u,(q `2 )) "\/" a )
reconsider u9 = u as Element of new_set2 A by XBOOLE_0:def 3;
ex u1 being Element of A st
( u1 = u9 & f . {A},u9 = (d . u1,(q `1 )) "\/" a ) by A17, A16;
hence f . {A},u = (d . u,(q `1 )) "\/" a ; :: thesis: f . {{A}},u = (d . u,(q `2 )) "\/" a
ex u2 being Element of A st
( u2 = u9 & f . {{A}},u9 = (d . u2,(q `2 )) "\/" a ) by A1, A16;
hence f . {{A}},u = (d . u,(q `2 )) "\/" a ; :: thesis: verum

end;

take f ; :: thesis: ( ( for u, v being Element of A holds f . u,v = d . u,v ) & f . {A},{A} = Bottom L & f . {{A}},{{A}} = Bottom L & f . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & f . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( f . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & f . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) )
A19: for u, v being Element of A holds f . u,v = d . u,v

proof

let u, v be Element of A; :: thesis: f . u,v = d . u,v
reconsider u9 = u, v9 = v as Element of new_set2 A by XBOOLE_0:def 3;
thus f . u,v = f . u9,v9
.= d . u,v by A16 ; :: thesis: verum

end;

for u being Element of A holds
( f . u,{A} = (d . u,(q `1 )) "\/" a & f . u,{{A}} = (d . u,(q `2 )) "\/" a )

proof

let u be Element of A; :: thesis: ( f . u,{A} = (d . u,(q `1 )) "\/" a & f . u,{{A}} = (d . u,(q `2 )) "\/" a )
reconsider u9 = u as Element of new_set2 A by XBOOLE_0:def 3;
ex u1 being Element of A st
( u1 = u9 & f . u9,{A} = (d . u1,(q `1 )) "\/" a ) by A17, A16;
hence f . u,{A} = (d . u,(q `1 )) "\/" a ; :: thesis: f . u,{{A}} = (d . u,(q `2 )) "\/" a
ex u2 being Element of A st
( u2 = u9 & f . u9,{{A}} = (d . u2,(q `2 )) "\/" a ) by A1, A16;
hence f . u,{{A}} = (d . u,(q `2 )) "\/" a ; :: thesis: verum

end;

hence ( ( for u, v being Element of A holds f . u,v = d . u,v ) & f . {A},{A} = Bottom L & f . {{A}},{{A}} = Bottom L & f . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & f . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( f . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & f . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) ) by A17, A1, A16, A19, A18; :: thesis: verum