reconsider a = q `3_4 , b = q `4_4 as Element of L ;
set x = q `1_4 ;
set y = q `2_4 ;
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_4),(q `2_4))) "\/" 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_4))) "\/" a ) ) & ( $1 in A & $2 = {{A}} implies ex p9 being Element of A st
( p9 = $1 & $3 = (d . (p9,(q `2_4))) "\/" a ) ) & ( $2 in A & $1 = {A} implies ex q9 being Element of A st
( q9 = $2 & $3 = (d . (q9,(q `1_4))) "\/" a ) ) & ( $2 in A & $1 = {{A}} implies ex q9 being Element of A st
( q9 = $2 & $3 = (d . (q9,(q `2_4))) "\/" 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, XREGULAR:7; :: 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_4),(q `2_4))) "\/" a) "/\" b ; :: thesis: S₁[p,q,((d . ((q `1_4),(q `2_4))) "\/" a) "/\" b]
thus S₁[p,q,((d . ((q `1_4),(q `2_4))) "\/" 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_4))) "\/" a ; :: thesis: S<sub>1</sub>[p,q,(d . (p9,(q `1_4))) "\/" a]
thus S₁[p,q,(d . (p9,(q `1_4))) "\/" 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_4))) "\/" a ; :: thesis: S<sub>1</sub>[p,q,(d . (p9,(q `2_4))) "\/" a]
thus S₁[p,q,(d . (p9,(q `2_4))) "\/" 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_4))) "\/" a ; :: thesis: S<sub>1</sub>[p,q,(d . (q9,(q `1_4))) "\/" a]
thus S₁[p,q,(d . (q9,(q `1_4))) "\/" 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_4))) "\/" a ; :: thesis: S<sub>1</sub>[p,q,(d . (q9,(q `2_4))) "\/" a]
thus S₁[p,q,(d . (q9,(q `2_4))) "\/" 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_4))) "\/" a & f . ({{A}},u) = (d . (u,(q `2_4))) "\/" a )

proof

let u be Element of A; :: thesis: ( f . ({A},u) = (d . (u,(q `1_4))) "\/" a & f . ({{A}},u) = (d . (u,(q `2_4))) "\/" 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_4))) "\/" a ) by A17, A16;
hence f . ({A},u) = (d . (u,(q `1_4))) "\/" a ; :: thesis: f . ({{A}},u) = (d . (u,(q `2_4))) "\/" a
ex u2 being Element of A st
( u2 = u9 & f . ({{A}},u9) = (d . (u2,(q `2_4))) "\/" a ) by A1, A16;
hence f . ({{A}},u) = (d . (u,(q `2_4))) "\/" 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_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & f . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & ( for u being Element of A holds
( f . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & f . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) )
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_4))) "\/" a & f . (u,{{A}}) = (d . (u,(q `2_4))) "\/" a )

proof

let u be Element of A; :: thesis: ( f . (u,{A}) = (d . (u,(q `1_4))) "\/" a & f . (u,{{A}}) = (d . (u,(q `2_4))) "\/" 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_4))) "\/" a ) by A17, A16;
hence f . (u,{A}) = (d . (u,(q `1_4))) "\/" a ; :: thesis: f . (u,{{A}}) = (d . (u,(q `2_4))) "\/" a
ex u2 being Element of A st
( u2 = u9 & f . (u9,{{A}}) = (d . (u2,(q `2_4))) "\/" a ) by A1, A16;
hence f . (u,{{A}}) = (d . (u,(q `2_4))) "\/" 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_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & f . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & ( for u being Element of A holds
( f . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & f . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) ) by A17, A1, A16, A19, A18; :: thesis: verum