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

proof

let p, q be Element of new_set A; :: thesis: ex r being Element of L st S₁[p,q,r]
A3: ( p in A or p in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;
A4: ( q in A or q in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;
A5: ( ( ( p = {A} or p = {{A}} or p = {{{A}}} ) & p = q ) iff ( ( p = {A} & q = {A} ) or ( 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}}} by TARSKI:def 1;
A10: ( A in {A} & {A} in {{A}} ) by TARSKI:def 1;
assume {{{A}}} in A ; :: thesis: contradiction
hence contradiction by A10, A9, ORDINAL1:4; :: thesis: verum

end;

A11: {A} <> {{{A}}}

proof

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

end;

A12: not {{A}} in A

proof

A13: ( A in {A} & {A} in {{A}} ) by TARSKI:def 1;
assume {{A}} in A ; :: thesis: contradiction
hence contradiction by A13, 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} & q = {{A}} ) or ( q = {A} & p = {{A}} ) or ( p = {A} & q = {{{A}}} ) or ( q = {A} & p = {{{A}}} ) or ( ( p = {A} or p = {{A}} or p = {{{A}}} ) & q = p ) or ( p in A & q = {A} ) or ( p in A & q = {{A}} ) or ( p in A & q = {{{A}}} ) or ( q in A & p = {A} ) or ( q in A & p = {{A}} ) or ( q in A & p = {{{A}}} ) ) by A3, A4, A5, ENUMSET1:def 1;

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, A12, A8; :: thesis: verum

end;

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

take a ; :: thesis: S₁[p,q,a]
thus S₁[p,q,a] by A7, A11, A12, A8, A14; :: thesis: verum

end;

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

take b ; :: thesis: S₁[p,q,b]
thus S₁[p,q,b] by A7, A11, A12, A15, TARSKI:def 1; :: thesis: verum

end;

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

take a "\/" b ; :: thesis: S₁[p,q,a "\/" b]
thus S₁[p,q,a "\/" b] by A7, A11, A8, A16, TARSKI:def 1; :: thesis: verum

end;

suppose A17: ( ( p = {A} or 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, A11, A12, A8, A17, TARSKI:def 1; :: thesis: verum

end;

suppose A18: ( 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 A11, A12, A8, A18, TARSKI:def 1; :: thesis: verum

end;

suppose A19: ( 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) "\/" b ; :: thesis: S<sub>1</sub>[p,q,((d . p9,(q `1 )) "\/" a) "\/" b]
thus S₁[p,q,((d . p9,(q `1 )) "\/" a) "\/" b] by A7, A12, A8, A19, TARSKI:def 1; :: thesis: verum

end;

suppose A20: ( 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 )) "\/" b ; :: thesis: S<sub>1</sub>[p,q,(d . p9,(q `2 )) "\/" b]
thus S₁[p,q,(d . p9,(q `2 )) "\/" b] by A7, A11, A12, A8, A20, TARSKI:def 1; :: thesis: verum

end;

suppose A21: ( 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 A11, A12, A8, A21, TARSKI:def 1; :: thesis: verum

end;

suppose A22: ( 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) "\/" b ; :: thesis: S<sub>1</sub>[p,q,((d . q9,(q `1 )) "\/" a) "\/" b]
thus S₁[p,q,((d . q9,(q `1 )) "\/" a) "\/" b] by A7, A12, A8, A22, TARSKI:def 1; :: thesis: verum

end;

suppose A23: ( 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 )) "\/" b ; :: thesis: S<sub>1</sub>[p,q,(d . q9,(q `2 )) "\/" b]
thus S₁[p,q,(d . q9,(q `2 )) "\/" b] by A7, A11, A12, A8, A23, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

proof

let u be Element of A; :: thesis: ( f . {A},u = (d . u,(q `1 )) "\/" a & f . {{A}},u = ((d . u,(q `1 )) "\/" a) "\/" b & f . {{{A}}},u = (d . u,(q `2 )) "\/" b )
reconsider u9 = u as Element of new_set A by XBOOLE_0:def 3;
ex u1 being Element of A st
( u1 = u9 & f . {A},u9 = (d . u1,(q `1 )) "\/" a ) by A26, A24;
hence f . {A},u = (d . u,(q `1 )) "\/" a ; :: thesis: ( f . {{A}},u = ((d . u,(q `1 )) "\/" a) "\/" b & f . {{{A}}},u = (d . u,(q `2 )) "\/" b )
ex u2 being Element of A st
( u2 = u9 & f . {{A}},u9 = ((d . u2,(q `1 )) "\/" a) "\/" b ) by A1, A24;
hence f . {{A}},u = ((d . u,(q `1 )) "\/" a) "\/" b ; :: thesis: f . {{{A}}},u = (d . u,(q `2 )) "\/" b
ex u3 being Element of A st
( u3 = u9 & f . {{{A}}},u9 = (d . u3,(q `2 )) "\/" b ) by A25, A24;
hence f . {{{A}}},u = (d . u,(q `2 )) "\/" b ; :: 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}}} = Bottom L & f . {{A}},{{{A}}} = q `3 & f . {{{A}}},{{A}} = q `3 & f . {A},{{A}} = q `4 & f . {{A}},{A} = q `4 & f . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & f . {{{A}}},{A} = (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 `1 )) "\/" (q `3 )) "\/" (q `4 ) & f . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & f . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) )
A28: 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_set A by XBOOLE_0:def 3;
thus f . u,v = f . u9,v9
.= d . u,v by A24 ; :: thesis: verum

end;

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

proof

let u be Element of A; :: thesis: ( f . u,{A} = (d . u,(q `1 )) "\/" a & f . u,{{A}} = ((d . u,(q `1 )) "\/" a) "\/" b & f . u,{{{A}}} = (d . u,(q `2 )) "\/" b )
reconsider u9 = u as Element of new_set A by XBOOLE_0:def 3;
ex u1 being Element of A st
( u1 = u9 & f . u9,{A} = (d . u1,(q `1 )) "\/" a ) by A26, A24;
hence f . u,{A} = (d . u,(q `1 )) "\/" a ; :: thesis: ( f . u,{{A}} = ((d . u,(q `1 )) "\/" a) "\/" b & f . u,{{{A}}} = (d . u,(q `2 )) "\/" b )
ex u2 being Element of A st
( u2 = u9 & f . u9,{{A}} = ((d . u2,(q `1 )) "\/" a) "\/" b ) by A1, A24;
hence f . u,{{A}} = ((d . u,(q `1 )) "\/" a) "\/" b ; :: thesis: f . u,{{{A}}} = (d . u,(q `2 )) "\/" b
ex u3 being Element of A st
( u3 = u9 & f . u9,{{{A}}} = (d . u3,(q `2 )) "\/" b ) by A25, A24;
hence f . u,{{{A}}} = (d . u,(q `2 )) "\/" b ; :: 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}}} = Bottom L & f . {{A}},{{{A}}} = q `3 & f . {{{A}}},{{A}} = q `3 & f . {A},{{A}} = q `4 & f . {{A}},{A} = q `4 & f . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & f . {{{A}}},{A} = (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 `1 )) "\/" (q `3 )) "\/" (q `4 ) & f . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & f . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) ) by A26, A1, A25, A24, A28, A27; :: thesis: verum