set M = Maximal_wrt F;
Maximal_wrt F is (M1) by Th28;
then ex A9, B9 being Subset of X st
( [A9,B9] >= [([#] X),([#] X)] & [A9,B9] in Maximal_wrt F ) ;
hence Maximal_wrt F is (C1) ; :: thesis: verum