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