let A be non empty finite set ; :: thesis:
let U be Function of (bool A),(bool A); :: thesis:
assume a0: ( U . {} = {} & ( for X being Subset of A holds (U . X) ` c= U . ((U . X) `) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) ) ; :: thesis:
then consider R being non empty finite RelStr such that
a1: ( the carrier of R = A & LAp R = Flip U & UAp R = U & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in U . {y} ) ) ) by YaoTh3;
set X = the carrier of R;
set I = the InternalRel of R;
for x, y being object st x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R holds
ex z being object st
( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R )

let x, y be object ; :: thesis:
assume W1: ( x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R ) ; :: thesis:
then reconsider xx = x, yy = y as Element of R ;
a3: ((UAp R) . {yy}) ` c= U . (((UAp R) . {yy}) `) by a0, a1;
not xx in (UAp R) . {yy} by W1, a1;
then xx in ((UAp R) . {yy}) ` by XBOOLE_0:def 5;
then xx in (UAp R) . (((UAp R) . {yy}) `) by a3, a1;
then xx in UAp (((UAp R) . {yy}) `) by ROUGHS_2:def 11;
then consider z being object such that
J1: ( z in Class ( the InternalRel of R,xx) & z in ((UAp R) . {yy}) ` ) by XBOOLE_0:3, ROUGHS_2:7;
reconsider zz = z as Element of R by J1;
J2: [xx,zz] in the InternalRel of R by J1, RELAT_1:169;
not zz in (UAp R) . {yy} by J1, XBOOLE_0:def 5;
then not [z,y] in the InternalRel of R by a1;
hence ex z being object st
( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) by J2; :: thesis:

end;