set R = the trivial Ring;
take the trivial Ring ; :: thesis: the trivial Ring is flat
thus the trivial Ring is flat by STRUCT_0:def 10; :: thesis: verum