let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2 d,q is symmetric
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2 d,q is symmetric
let d be BiFunction of A,L; :: thesis: ( d is symmetric implies for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2 d,q is symmetric )
assume A1: d is symmetric ; :: thesis: for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2 d,q is symmetric
let q be Element of [:A,A,the carrier of L,the carrier of L:]; :: thesis: new_bi_fun2 d,q is symmetric
set f = new_bi_fun2 d,q;
set x = q `1 ;
set y = q `2 ;
set a = q `3 ;
set b = q `4 ;
let p, q be Element of new_set2 A; :: according to LATTICE5:def 6 :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p
A2: ( p in A or p in {{A},{{A}}} ) by XBOOLE_0:def 3;
A3: ( q in A or q in {{A},{{A}}} ) by XBOOLE_0:def 3;

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

suppose ( p in A & q in A ) ; :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p

then reconsider p9 = p, q9 = q as Element of A ;
thus (new_bi_fun2 d,q) . p,q = d . p9,q9 by Def5
.= d . q9,p9 by A1, LATTICE5:def 6
.= (new_bi_fun2 d,q) . q,p by Def5 ; :: thesis: verum

end;

suppose A4: ( p in A & q = {A} ) ; :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p

then reconsider p9 = p as Element of A ;
thus (new_bi_fun2 d,q) . p,q = (d . p9,(q `1 )) "\/" (q `3 ) by A4, Def5
.= (new_bi_fun2 d,q) . q,p by A4, Def5 ; :: thesis: verum

end;

suppose A5: ( p in A & q = {{A}} ) ; :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p

then reconsider p9 = p as Element of A ;
thus (new_bi_fun2 d,q) . p,q = (d . p9,(q `2 )) "\/" (q `3 ) by A5, Def5
.= (new_bi_fun2 d,q) . q,p by A5, Def5 ; :: thesis: verum

end;

suppose A6: ( p = {A} & q in A ) ; :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p

then reconsider q9 = q as Element of A ;
thus (new_bi_fun2 d,q) . p,q = (d . q9,(q `1 )) "\/" (q `3 ) by A6, Def5
.= (new_bi_fun2 d,q) . q,p by A6, Def5 ; :: thesis: verum

end;

suppose ( p = {A} & q = {A} ) ; :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p

hence (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p ; :: thesis: verum

end;

suppose A7: ( p = {A} & q = {{A}} ) ; :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p

hence (new_bi_fun2 d,q) . p,q = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) by Def5
.= (new_bi_fun2 d,q) . q,p by A7, Def5 ;
:: thesis: verum

end;

suppose A8: ( p = {{A}} & q in A ) ; :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p

then reconsider q9 = q as Element of A ;
thus (new_bi_fun2 d,q) . p,q = (d . q9,(q `2 )) "\/" (q `3 ) by A8, Def5
.= (new_bi_fun2 d,q) . q,p by A8, Def5 ; :: thesis: verum

end;

suppose A9: ( p = {{A}} & q = {A} ) ; :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p

hence (new_bi_fun2 d,q) . p,q = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) by Def5
.= (new_bi_fun2 d,q) . q,p by A9, Def5 ;
:: thesis: verum

end;

suppose ( p = {{A}} & q = {{A}} ) ; :: thesis: (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p

hence (new_bi_fun2 d,q) . p,q = (new_bi_fun2 d,q) . q,p ; :: thesis: verum

end;

end;